$\forall$$A$,$B$:Type, $a$:EqDecider($A$), $b$:EqDecider($B$). sumdeq($a$; $b$) $\in$ ($A$ + $B$)$\rightarrow$($A$ + $B$)$\rightarrow\mathbb{B}$